$\forall$$M_{1}$, $M_{2}$:MsgA.
\\[0ex]$M_{1}$ $\subseteq$ $M_{2}$
\\[0ex]$\Rightarrow$ ($\forall$$k$:Knd, $l$:IdLnk, ${\it tg}$:Id. $M_{2}$.sframe($k$ sends $<$$l$,${\it tg}$$>$) $\Rightarrow$ $M_{1}$.sframe($k$ sends $<$$l$,${\it tg}$$>$))